        bits 64
        
        db 0xc4, 0x62, 0x7f, 0xcb, 0xc7         ; VSHA512RNDS2 ymm8, ymm0, xmm7
        db 0xc4, 0x62, 0x7f, 0xcc, 0xc7         ; VSHA512MSG1 ymm8, xmm7
        db 0xc4, 0x62, 0x7f, 0xcd, 0xc7         ; VSHA512MSG2 ymm8, ymm7
        db 0xc4, 0x63, 0x79, 0xde, 0xc7, 0xef   ; VSM3RNDS2 xmm8, xmm0, xmm7, 0xef
        db 0xc4, 0x63, 0x79, 0xde, 0x01, 0xef   ; VSM3RNDS2 xmm8, xmm0, xmmword ptr [rcx], 0xef